; Copyright (c) 2016 Microsoft Corporation
(declare-const a String)
(declare-const b String)
(declare-const c String)
(declare-const d String)
(declare-const e String)


(push)
(set-info :status sat)
(assert (= a "a"))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= a (str.++ "a" "b")))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= a b))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (not (= a b)))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (not (= a "a")))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= a (str.++ a "a")))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= b (str.++ a "a")))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= (str.++ a b) (str.++ b "a" a)))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= (str.++ a "b") (str.++ "a" a)))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= (str.++ a "b") (str.++ "a" a)))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= a (str.++ b "a" c "b" d)))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= a (str.++ b "a" c "b" a)))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= a "ab"))
(assert (= (str.++ a b) "abcd"))
(check-sat)
(get-model)
(pop)


(push)
(set-info :status sat)
(assert (= a "ab"))
(assert (= (str.++ a b) "abcd"))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= a "cd"))
(assert (= (str.++ b a) "abcd"))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= b "cd"))
(assert (= (str.++ a b c) "abcdef"))
(check-sat)
(get-model)
(pop)





(push)
(set-info :status sat)
(assert (= (str.++ a b) ""))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) "a"))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) "ab"))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) "abcd"))
(assert (= (str.++ b c) "cdef"))
(assert (not (= b "")))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) c))
(assert (or (= a "ab") (= a "bc") (= a "de")))
(assert (or (= c "aab") (= c "abc") (= c "ade")))
(check-sat)
;(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abc" a) (str.++ "abc" b)))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abc" a) (str.++ "abcd" b)))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abcd" a) (str.++ "abc" b)))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= (str.++ "abc" a) (str.++ "xbc" b)))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abc" a) (str.++ b "def")))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abc" a) (str.++ b "cef")))
(check-sat)
(pop)



; ---- test interaction with length constraints ---

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ c d e)))
(assert (= (str.len a) (str.len b)))
(check-sat)
;(get-model)
(pop)


(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ c d e)))
(assert (= (str.len a) (str.len b)))
(assert (not (= a "")))
(check-sat)
;(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ c d e)))
(assert (= (str.len a) (str.len b)))
(assert (> (str.len a) 1))
(check-sat)
;(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) c))
(assert (= (str.len a) 0))
(assert (= (str.len b) 2))
(check-sat)
;(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) c))
(assert (= (str.len a) 2))
(assert (= (str.len b) 0))
(check-sat)
;(get-model)
(pop)


(push)
(set-info :status sat)
(assert (= (str.++ a b) c))
(assert (= (str.len a) 2))
(assert (= (str.len b) 1))
(check-sat)
;(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ "a" c)))
(assert (= (str.len a) 0))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ "a" c)))
(assert (= (str.len b) 0))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ "a" c)))
(assert (= (str.len c) 0))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ "a" c)))
(assert (= (str.len c) 0))
(assert (= (str.len a) 0))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a b) (str.++ "a" c)))
(assert (= (str.len c) 0))
(assert (= (str.len b) 0))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= (str.++ a b) (str.++ "a" c)))
(assert (= (str.len a) 0))
(assert (= (str.len b) 0))
(check-sat)
(pop)


(push)
(set-info :status sat)
(assert (= (str.++ a "b" b) (str.++ "a" c)))
(assert (= (str.len a) 3))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ a "b" b) (str.++ "a" c)))
(assert (= (str.len b) 3))
(check-sat)
(pop)


(push)
(set-info :status sat)
(assert (= (str.++ a "b" b) (str.++ "a" c)))
(assert (= (str.len c) 3))
(check-sat)
(pop)


(push)
(set-info :status sat)
(assert (= (str.++ a "b" b) (str.++ "a" c)))
(assert (= (str.len c) 2))
(check-sat)
(pop)


(push)
(set-info :status sat)
(assert (= (str.++ a "b" b) (str.++ "a" c)))
(assert (= (str.len c) 1))
(check-sat)
(pop)


(push)
(set-info :status unsat)
(assert (= (str.++ a "b" b) (str.++ "a" c)))
(assert (= (str.len c) 0))
(check-sat)
(pop)



(push)
(set-info :status unsat)
(assert (= (str.++ "abc" a) (str.++ b "cef")))
(assert (= (str.len a) 1))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abc" a) (str.++ b "cef")))
(assert (= (str.len a) 2))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= (str.++ "abc" a) (str.++ b "cef")))
(assert (>= (str.len a) 3))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= (str.++ a "b") (str.++ b "c" d)))
(assert (= (str.len a) 0))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (not (= (= a "") (= (str.len a) 0))))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= c (str.++ "a" b)))
(assert (= c (str.++ a "b")))
(assert (= (str.len a) 1))
(check-sat)
;(get-model)
(pop)

(push)
(set-info :status sat)
(assert (= e (str.++ a "bc")))
(assert (= e (str.++ b c)))
(assert (= e (str.++ "ab" d)))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= e (str.++ a "abc" b)))
(assert (= e (str.++ c "ef" d)))
(assert (= (str.len e) 4))
(check-sat)
(pop)

(push)
(set-info :status unsat)
(assert (= e (str.++ a "abc" b)))
(assert (= e (str.++ c "ef" d)))
(assert (<= (str.len e) 4))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= e (str.++ a "abc" b)))
(assert (= e (str.++ c "ef" d)))
(assert (= (str.len e) 5))
(check-sat)
(pop)


(push)
(set-info :status sat)
(assert (= e (str.++ a "abc" b)))
(assert (= e (str.++ c "ef" d)))
(assert (= (str.len e) 6))
(check-sat)
(pop)

(push)
(set-info :status sat)
(assert (= e (str.++ a "abc" b)))
(assert (= e (str.++ c "ef" d)))
(assert (>= (str.len e) 6))
(check-sat)
(pop)

(push)
(set-info :status sat)
 (assert (= (str.++ a "ab") (str.++ "ba" a)))
 (assert (= (str.len a) 7))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status unsat)
 (assert (= (str.++ a "ab") (str.++ "ba" a)))
 (assert (= (str.len a) 6))
(check-sat)
(pop)

 

(push)
(set-info :status sat) 
 (assert (not (=  a b)))
 (assert (= (str.len a) (str.len b))) 
 (check-sat)
(pop)

(push)
 (set-info :status sat)
 (assert (not (= (str.++ c a b) (str.++ b a))))
 (check-sat)
(pop)

(push)
 (set-info :status sat)
 (assert (= (str.++ a "ab" b) (str.++ b "ba" c)))
 (assert (= c (str.++ a b)))
 (assert (not (= (str.++ a "a") (str.++ "a" a))))
 (check-sat)
(pop)